// SPDX-License-Identifier: GPL-2.0 or GPL-3.0
// Copyright © 2019 Ariadne Devos

#ifndef _sHT_ARCH_MINMAX
#define _sHT_ARCH_MINMAX

/* Operational semantics: If %0 > %1, do %0 <- %1.
  Functional semantics:

  In case \old(%0) > \old(%1) (branch taken),
  - \old(%1) = min(\old(%0), \old(%1)) (case analysis)
  - \new(%0) = \old(%1) = min(\old(%0), \old(%1)) (assignment, previous lemma)
  Otherwise, the negation holds: \old(%0) ⩽ \old(%1),
  - \old(%0) = min(\old(%0), \old(%1)) (case analysis)
  - \new(%0) = \old(%0) = min(\old(%0), \old(%1)) (no assignment, previous lemma)

  Therefore, \new(%0) = min(\old(%0), \old(%1)) (consider both branches).

  %0 is a register, %1 an Operand2
  %1 may alias to %0, in which case the operation is pointless but correct.
  cc: condition code is changed by 'cmp' and 'mov'. */
#define _sHT_min(x_set_p, y) \
	__asm__("cmp %0,%1;movhi %0,%1" : "+r" (*(x_set_p)) : "r" (y) : "cc")

#endif
